Using the verification prototype, we generated a transformation model, a USE
specification, and a search configuration (as shown in Fig.
~\ref{fig:toolchain}). After adding the constraints (Table \ref{tab:OCLConsts})
to the USE specification, we ran the USE tool once for each constraint.

Out of the 18 constraints in Table \ref{tab:OCLConsts}, only two multiplicity
invariants were found to be violated by the transformation:
$\mathtt{CompositionType\_component}$ and $\mathtt{SwcToEcuMapping\_component}$.
In other words, our transformation can generate a \emph{CompositionType} with no
\emph{ComponentPrototype}s and/or a \emph{SwcToEcuMapping} with no
\emph{ComponentPrototype}s. Both of these possible outputs violate the
multiplicities defined in the AUTOSAR metamodel (Figure \ref{fig:systempfig}).

After examining the two counterexamples generated by USE for the two violated
constraints, we identified two bugs in two rules shown in Table
~\ref{tab:buggyRules}:
$\mathtt{initSysTemp}$ and $\mathtt{initSingleSwc2EcuMapping}$. The bold,
underlined text are the updates to the rules that address the two
bugs. $\mathtt{initSysTemp}$ initially mapped a \emph{PhysicalNode} to many
elements, including a \emph{CompositionType} that must contain atleast one
\emph{ComponentPrototype}. If the \emph{PhysicalNode} did not have any
\emph{Module} in any of its \emph{Partition}s, then the created
\emph{CompositionType} will not contain any \emph{ComponentPrototype}s. Thus we
added a matching constraint to the \emph{PhysicalNode} matched by the rule to
ensure that any of its \emph{Partition}s must contain atleast one \emph{Module}.
Similarly, $\mathtt{initSingleSwc2EcuMapping}$ initially mapped a
\emph{Partition} to a \emph{SwcToEcuMapping} that must contain atleast one
\emph{SwCompToEcuMapping\_component}. If the \emph{Partition} didnot have any
\emph{Module}, then the created \emph{SwcToEcuMapping} will not contain any
\emph{SwCompToEcuMapping\_component}. Thus we added a matching constraint to the
\emph{Partition} matched by the rule to ensure that it must contain atleast one
\emph{Module}.

The 18 constraints were reverified on the updated
transformation, and were all found to be preserved.
% \begin{figure*}[tbh]
%  \resizebox{0.8\textwidth}{2.0cm}{%{0.8\textwidth}{!} %2.4cm
%   \includegraphics{imgs/buggyRules.jpg}
%  }
% \caption{The two transformation rules that required changes to address
% violations in multiplicity invariants.}
% \label{fig:buggyRules}
% \vspace{-0.6cm}
% \end{figure*}
\begin{table}[!h]%tbh
\vspace{-0.6cm}
 	\centering
 	\scriptsize%\tiny%\scriptsize%\footnotesize
 	\renewcommand{\arraystretch}{1} %was 2.4, 1.5
\begin{tabular}{|p{12.2cm}|}
\hline
rule initSysTemp\{

from  ph: GM!PhysicalNode
{\underline{{\bf{(ph.partition$\mathtt{\to}$exists(p$\mathtt{\mid}$p.Module$\mathtt{\to}$notEmpty()))}}}}

to 

\ldots 

compostype:autosar!CompositionType(
           
           \ldots
           
           component $\mathtt{\gets}$
           ph.partition$\mathtt{\to}$collect(p$\mathtt{\mid}$
           p.Module)$\mathtt{\to}$flatten()$\mathtt{\to}$collect(m$\mathtt{\mid}$
           thisModule.resolveTemp(m, 'comp'))) \}
\\ \hline
rule initSingleSwc2EcuMapping \{ 

from p:GM!Partition

((GM!PhysicalNode.allInstances()$\mathtt{\to}$one(ph$\mathtt{\mid}$
ph.partition$\mathtt{\to}$includes(p))) {\underline{{\bf{and
(p.module$\mathtt{\to}$notEmpty()))}}}}    

to mapping:autosar!SwcToEcuMapping (
           
           shortName  $\mathtt{\gets}$ p.Name,
           
            component $\mathtt{\gets}$ p.Module
           $\mathtt{\to}$collect(m$\mathtt{\mid}$thisModule.resolveTemp(m, 'mapComp')),
           
           ecuInstance $\mathtt{\gets}$
           thisModule.resolveTemp((GM!PhysicalNode.allInstances()$\mathtt{\to}$
           select(ph$\mathtt{\mid}$
           ph.partition$\mathtt{\to}$includes(p)))$\mathtt{\to}$first(),'EcuInst'))\}
           \\ \hline 
 \end{tabular}
\caption{The two rules that required updates to address the two violations of
multiplicity invariants.}
\label{tab:buggyRules}
\vspace{-1cm}
\end{table} 